Nuprl Lemma : fun_exp_add
11,40
postcript
pdf
T
:Type,
n
,
m
:
,
f
:(
T
T
).
f
^
n
+
m
= (
f
^
n
o
f
^
m
)
T
T
latex
Definitions
P
Q
,
P
&
Q
,
t
T
,
P
Q
,
P
Q
,
f
^
n
,
x
:
A
.
B
(
x
)
,
Lemmas
int
seg
wf
,
compose
wf
,
primrec
add
,
fun
exp
compose
,
fun
exp
wf
,
nat
wf
origin